Nuprl Lemma : gcd_assoc
2,24
postcript
pdf
a
,
b
,
c
:
. gcd(gcd(
a
;
b
);
c
) ~ gcd(
a
;gcd(
b
;
c
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
gcd(
a
;
b
)
,
P
Q
,
GCD(
a
;
b
;
y
)
,
P
&
Q
,
a
~
b
Lemmas
gcd
of
triple
,
gcd
p
sym
,
gcd
p
wf
,
gcd
wf
,
gcd
sat
pred
origin
a, b, c:
. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)) a, b, c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)) x:A. B(x)
T
Q